A. Technical Field
This invention pertains to equivalency checking techniques that verify the design of a power optimized digital integrated circuit, system-on-chip (SOC), or other electronic design.
B. Background of the Invention
Equivalency checking is an important application of formal verification techniques in the semiconductor industry. Replacing millions of simulation cycles, equivalency checking is used to demonstrate the correctness of RTL synthesis results and gate-level optimizations. One example application of equivalency checking is to verify functional equivalence of combinational circuits after multi-level logic synthesis. In a typical scenario, there are two structurally different implementations of the same design, and the problem is to prove their functional equivalence.
Equivalency checking is either combinational or sequential. In combinational equivalency checking only the combinational portions of the two designs are compared, and implications about the sequential behavior are derived by establishing a 1-to-1 mapping between the register inputs and outputs of the two designs. The reduction from sequential to combinational reasoning makes the checking problem easier but relies on the construction of a mapping between registers. Register mappings can often be constructed partially or fully in an automatic fashion, and for designs with aggressive register optimizations, deriving the register mappings is not a trivial process. In sequential equivalency checking, the full combinational and sequential behavior is considered together. Sequential equivalency checking is computationally harder than combinational checking and does not require a 1-to-1 correspondence in register mappings. In fact, the term sequential is only used to explicitly distinguish from combinational equivalency checking which due to its widespread use has become synonymous with equivalency checking.
If one considers an implementation of the original design and an alternate implementation of the original design, then equivalency checking is the analysis of the structural differences between the two implementations and the determination of their equivalence. Several electronic design automation companies, including Cadence, Synopsys, Calypto, and Magma Design Automation, offer products that provide equivalency checking capability. These equivalency checking products give consistent results when analyzing the functionality of the original design against the functionality of alternate implementations of the design.
Functional equivalency checking is used to check whether two designs are functionally equivalent; that is, on the same input sequences they both produce the same output sequences. The equivalence is said to be functional because it is only concerned with logical behavior and not necessarily aware of technology dependent factors such as speed, area, and power consumption. Though cost efficient, the application of equivalency checking requires both a certain amount of know-how and a fair amount of setup to be successful.
As low power consumption becomes a critical requirement in many designs, power optimizations will have to be provided in early phases of the design. In generating such power-optimized versions of an original design, it is imperative that the functional behavior of the design is unchanged. Thus, a method and apparatus for automating the verification of power optimized designs will be desirable.